A:Type, eq:EqDecider(A), B:(AType), g:x:A fp B(x), x:A.
x  dom(fpf-normalize(eq;g)) ~ x  dom(g) 

latex

Definitions

t  T, Void, x:A. B(x), x:AB(x), P  Q, x:A. B(x), x  dom(f), , f  g, x : v, fpf-normalize(eq;g), x:AB(x), a:A fp B(a), Type, EqDecider(T), f(a), x(s), x. t(x), Top, s = t, nil, false, eqof(d), p  q, b, x.A(x), filter(P;l), car.cdr, reduce(f;k;as), , <a,b>, f(x), f(x)?z, 1of(t), s ~ t, deq-member(eq;x;L), , {T}, SQType(T), b, A, Prop, P & Q, P  Q, Unit, left+right, type List, False, true, p  q, (x  l), True, P  Q

Lemmas

assert of band, and functionality wrt iff, true wf, filter functionality, bnot thru bor, assert-deq-member, deq-member wf, not functionality wrt iff, member filter, l member wf, band wf, btrue wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, not wf, assert wf, bool wf, bool sq, reduce wf, filter wf, bnot wf, bor wf, eqof wf, bfalse wf, fpf wf, deq wf, top wf